Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use llvm_points_to_bitfield in SAW proofs #3155

Merged
merged 5 commits into from
Jan 29, 2022
Merged

Use llvm_points_to_bitfield in SAW proofs #3155

merged 5 commits into from
Jan 29, 2022

Conversation

RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Dec 15, 2021 •
edited
Loading

Resolved issues:

This concludes a line of discussion that was started as a review comment in #3079 (comment).

Description of changes:

The main commit in this PR is:

Use llvm_points_to_bitfield in SAW proofs

This uses SAW's new llvm_points_to_bitfield command (introduced in GaloisInc/saw-script#1539) to simplify specifications that involve the bitfields in s2n_config and s2n_connection. In particular, there is no longer any need to manually compute the size of the bitfields or the indices of the fields within the bitfields, as these details are handled automatically by llvm_points_to_bitfield. The positions of the fields within bitfields are also no longer important.

Call-outs:

  • The first commit changes all of the proof tactics in handshake.saw to What4-based tactics (e.g., w4_unint_yices), as llvm_points_to_bitfield only supports What4-based tactics at present.
  • Similarly, handshake_io_lowlevel.saw uses the enable_lax_loads_and_stores SAW command, as that is required to make llvm_points_to_bitfield work properly.

Testing:

There is no real change in functionality in this PR, just refactoring. As a result, the existing SAW CI is sufficient to test these changes. The only change to the C code is to delete obsolete comments, which should have no change in behavior on the C side of things.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

@RyanGlScott
Copy link
Contributor Author

I've marked this PR as a draft for now since I still need to update the CI to use a more recent version of SAW with the changes in GaloisInc/saw-script#1539. I am currently preparing a SAW bindist with these changes, but in the meantime, any review comments would be appreciated.

@dougch
Copy link
Contributor

dougch commented Dec 15, 2021

Benchmark report
No change in performance detected.

@feliperodri feliperodri added the SAW Anything related to SAW proofs. label Dec 15, 2021
@dougch
Copy link
Contributor

dougch commented Jan 4, 2022

Benchmark report
No change in performance detected.

@RyanGlScott RyanGlScott changed the title Draft: Use llvm_points_to_bitfield in SAW proofs Use llvm_points_to_bitfield in SAW proofs Jan 4, 2022
@RyanGlScott
Copy link
Contributor Author

I've pushed a commit which adjusts the CI to use a nightly version of SAW that includes GaloisInc/saw-script#1539. The AWS CodeBuild BuildBatch us-west-2 (s2nIntegrationBatch) job now fails, but I'm not entirely sure why.

@RyanGlScott RyanGlScott marked this pull request as ready for review January 4, 2022 20:40
@dougch dougch requested a review from lrstewart January 5, 2022 18:18
@dougch
Copy link
Contributor

dougch commented Jan 5, 2022

The AWS CodeBuild BuildBatch us-west-2 (s2nIntegrationBatch) job now fails, but I'm not entirely sure why.

It passed on a retry

@dougch
Copy link
Contributor

dougch commented Jan 5, 2022

Benchmark report
No change in performance detected.

lrstewart
lrstewart reviewed Jan 10, 2022
View reviewed changes
Copy link
Contributor

@lrstewart lrstewart left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like the proofs now run in <3min with the newest version of SAW. Nice!

tests/saw/spec/handshake/handshake.saw Outdated Show resolved Hide resolved
tls/s2n_connection.h Outdated Show resolved Hide resolved
@dougch
Copy link
Contributor

dougch commented Jan 10, 2022

Benchmark report
No change in performance detected.

@dougch
Copy link
Contributor

dougch commented Jan 10, 2022

Benchmark report
No change in performance detected.

@dougch
Copy link
Contributor

dougch commented Jan 24, 2022

Benchmark report
No change in performance detected.

@RyanGlScott
Copy link
Contributor Author

I must have bad luck with the CI lottery, since I can't seem to get the AWS CodeBuild BuildBatch us-west-2 (s2nGeneralBatch) job to pass. The job failure looks unrelated to the changes in this PR:

--> Finished Dependency Resolution
Error: Package: 1:nodejs-16.13.2-3.el7.x86_64 (epel)
           Requires: libuv >= 1:1.42.0
           Installed: 1:libuv-1.39.0-1.amzn2.x86_64 (@amzn2-core)
               libuv = 1:1.39.0-1.amzn2
           Available: 1:libuv-1.23.2-1.amzn2.0.2.i686 (amzn2-core)
               libuv = 1:1.23.2-1.amzn2.0.2
 You could try using --skip-broken to work around the problem
 You could try running: rpm -Va --nofiles --nodigest

@dougch
Copy link
Contributor

dougch commented Jan 26, 2022

Benchmark report
No change in performance detected.

@RyanGlScott
Copy link
Contributor Author

With that rebase, all the CI jobs are finally green.

Is there anything else that should be done before this can be merged?

@dougch
Copy link
Contributor

dougch commented Jan 26, 2022

With that rebase, all the CI jobs are finally green.

Is there anything else that should be done before this can be merged?

Added an approval, but it needs one more pass.

@dougch
Copy link
Contributor

dougch commented Jan 26, 2022

Benchmark report
No change in performance detected.

@dougch
Copy link
Contributor

dougch commented Jan 26, 2022

Benchmark report
No change in performance detected.

@RyanGlScott
Copy link
Contributor Author

Added an approval, but it needs one more pass.

Ah, OK! After rebasing once more, I've achieved another round of all-green CI jobs.

@dougch
Copy link
Contributor

dougch commented Jan 27, 2022

Benchmark report
No change in performance detected.

@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
1270e70 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
@RyanGlScott
Remove obsolete comments about bitfield flag ordering
6a10dbc 
These comments are no longer relevant now that the SAW proofs use the
`llvm_bitfield_points_to` command, which is insensitive to the order of fields
within a bitfield.
@RyanGlScott
ci: Use SAW-0.9.0.99 nightly bindist
bbc1356
@dougch
Copy link
Contributor

dougch commented Jan 27, 2022

Benchmark report
No change in performance detected.

@dougch
Copy link
Contributor

dougch commented Jan 27, 2022

Benchmark report
No change in performance detected.

@dougch
Copy link
Contributor

dougch commented Jan 27, 2022

Benchmark report
No change in performance detected.

@RyanGlScott
Copy link
Contributor Author

Hm. I keep encountering (seemingly transient) errors whenever I try to restart the CI. I've tried restarting about 3 times, but with no luck today. Any ideas on what might be causing this?

@dougch
Copy link
Contributor

dougch commented Jan 28, 2022

Benchmark report
No change in performance detected.

@lrstewart lrstewart merged commit 7f1017e into aws:main Jan 29, 2022
@RyanGlScott
Copy link
Contributor Author

Thanks, everyone!

RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Jan 31, 2022
@RyanGlScott
Bump s2n commit in Dockerfile
5bf89a1 
This bumps the `s2n` commit to
GaloisInc/s2n@7f1017e, which points to the
`llvm_points_to_bitfield` changes that were merged into the upstream `s2n-tls`
repo in aws/s2n-tls#3155.
@RyanGlScott RyanGlScott mentioned this pull request Jan 31, 2022
Draft
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 1, 2022
@RyanGlScott
Bump s2n commit in Dockerfile
0e8e547 
This bumps the `s2n` commit to
GaloisInc/s2n@7f1017e, which points to the
`llvm_points_to_bitfield` changes that were merged into the upstream `s2n-tls`
repo in aws/s2n-tls#3155.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 8, 2022
@RyanGlScott
Bump s2n commit in Dockerfile
0829f4b 
This bumps the `s2n` commit to
GaloisInc/s2n@7f1017e, which points to the
`llvm_points_to_bitfield` changes that were merged into the upstream `s2n-tls`
repo in aws/s2n-tls#3155.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Mar 21, 2022
@RyanGlScott
Bump s2n commit in Dockerfile
ad2b908 
This bumps the `s2n` commit to
GaloisInc/s2n@7f1017e, which points to the
`llvm_points_to_bitfield` changes that were merged into the upstream `s2n-tls`
repo in aws/s2n-tls#3155.
@RyanGlScott RyanGlScott mentioned this pull request Apr 19, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lrstewart lrstewart lrstewart approved these changes

@dougch dougch dougch approved these changes

Assignees

@RyanGlScott RyanGlScott

Labels
SAW Anything related to SAW proofs.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@RyanGlScott @dougch @lrstewart @feliperodri